$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)), ${\it Config}$:AbsInterface(chain\_config()).
\\[0ex]E(${\it Sys}$(valid)) $\subseteq$r E(${\it Sys}$)